There Is No Preview Available For This Item
This item does not appear to have any files that can be experienced on Archive.org.
Please download files in this item to interact with them on your computer.
Show all files
In all sound program analysis systems there is some mechanism for modeling non-deterministic choice, which is typically used to correctly capture effects of the program's environment (Did malloc return a valid pointer or null? Which thread did the scheduler pick?) and imprecision in the analysis (Which element was read by the array reference? Is a certain key in the hash map?). In constraint-based analyses it is common to model such decisions as an unconstrained variable ranging over the possible outcomes (e.g., malloc returned either null or a pointer, but not both). Unfortunately, this very useful idea leads to both theoretical and practical difficulties. On the theoretical side, each choice should introduce a fresh variable, leading to a potentially unbounded number of variables in recursive procedures; practically, even in relatively small, non-recursive problems the number of such variables imposes real limits on scalability.
In this talk we present a solution to both the theoretical and practical problems. Given a (recursive) formula F with variables representing non-deterministic choices, we eliminate such variables in favor of two formulas capturing upper and lower bounds on F: the strongest necessary and weakest sufficient conditions under which the original formula was satisfiable and valid, respectively. These formulas are satisfiable/valid exactly when F is, so there is no loss of information in the transformation, and in practice these formulas are much smaller than F. We apply this idea to SAT-based path- and context-sensitive program analysis and demonstrate the practicality of the approach by analyzing programs as large as the entire Linux kernel.